css: Convert numbers with GTK's dpi
authorBenjamin Otte <otte@redhat.com>
Fri, 5 Feb 2016 13:50:37 +0000 (14:50 +0100)
committerBenjamin Otte <otte@redhat.com>
Fri, 5 Feb 2016 13:52:09 +0000 (14:52 +0100)
commit5444442974f55df857b0c5169e481ac8abc93ea7
tree488e091546f2d46b14d100290bc69f2a94eb9834
parente35e6abbb2ea824afd6db2d54d10666cd23ad54c
css: Convert numbers with GTK's dpi

Don't hardcode 96 for dpi, but instead use the value of the -gtk-dpi
property (that mirrors the GdkScreen's dpi if it wasn't set explicitly).

This makes these values scale when the large font setting in
control-center is enabled.
gtk/gtkcssnumbervalue.c